Nuprl Lemma : grp_op_preserves_lt_qorder
11,40
postcript
pdf
u
,
v
,
w
:
.
v
<
w
u
+
v
<
u
+
w
latex
Definitions
t
T
,
t
.2
,
t
.1
,
OGrp
,
<
+>
,
*
,
x
f
y
,
|
g
|
,
x
:
A
.
B
(
x
)
,
r
<
s
Lemmas
ocgrp
wf
,
qadd
grp
wf2
,
grp
op
preserves
lt
origin
u, v, w:
. v < w 
u + v < u + w u, v, w:. v < w u + v < u + w 
T+>x:A. B(x)